FDL - Nuprl Lemma : interleaving_split

Nuprl Lemma : interleaving_split

T:Type, L:T List, P:(

||L||

Prop).
(

x:

||L||. Dec(P(x)))

(

L1, L2:T List, f1:(

||L1||

||L||), f2:(

||L2||

||L||).

(interleaving_occurence(T;L1;L2;L;f1;f2)

(& (

i:

||L1||. P(f1(i))) & (

i:

||L2||.

P(f2(i)))

(& (

i:

||L||.

(& ((P(i)

(

j:

||L1||. f1(j) = i

)) & (

P(i)

(

j:

||L2||. f2(j) = i

))))

Definitions T, P Q, {T}, SQType(T), True, sublist_occurence(T;L1;L2;f), i j < k, S T, S T, A & B, P & Q, x:A. B(x), t T, x:A. B(x), ij, P Q, False, A, AB, , Prop, {i..j}, Dec(P), interleaving_occurence(T;L1;L2;L;f1;f2), ||as||

Lemmas decidable wf, int seg wf, increasing split, length wf1, non neg length, range sublist, le wf, interleaving occurence wf, not wf, disjoint increasing onto